Inference at * 1 1 2 
Iof proof for Lemma fun with inv is bij:



1. A : Type
2. B : Type
3. f : AB
4. g : BA
5. (g o f) = Id{A}
6. (f o g) = Id{B}
7. b : B
  a:A. (f(a) = b) 

latex

 by ((With g(b) (D 0)) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   f(g(b)) = b
C.

Definitions

, t  T, x:A. B(x)